Nuprl Definition : Rusends1
11,40
postcript
pdf
k
(v) sends [
tg
,
f
(State(
ds
), v)] on
l
== Rsends(
ds
;
k
;
A
;
l
;
tg
:
T
;[<
tg
,
s
,
v
. [(
f
(
s
,
v
))]>])
latex
clarification:
Rusends1(
ds
;
k
;
A
;
l
;
tg
;
T
;
f
) == Rsends(
ds
;
k
;
A
;
l
;
tg
:
T
;[<
tg
,
s
,
v
. [(
f
(
s
,
v
)) / []]> / []])
latex
Definitions
Rsends(
ds
;
knd
;
T
;
l
;
dt
;
g
)
,
x
:
v
,
<
a
,
b
>
,
x
.
A
(
x
)
,
[
car
/
cdr
]
,
f
(
a
)
,
[]
FDL editor aliases
Rusends1
origin
s,v. [(f(s,v))]>])
s,v. [(f(s,v)) / []]> / []]) s,v. [(f(s,v))]>])
s,v. [(f(s,v)) / []]> / []]) x.A(x)